Nuprl Lemma : atom-deq_wf
0,22
postcript
pdf
AtomDeq
EqDecider(Atom)
latex
Definitions
EqDecider(
T
)
,
AtomDeq
,
atom-deq-aux
,
x
=
y
Atom
,
P
Q
,
Prop
,
b
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
assert
wf
,
iff
wf
,
eq
atom
wf
,
atom-deq-aux
origin
EqDecider(Atom) EqDecider(Atom) 
yAtom
Q
b
x:A. B(x) T